retraction($T$;$f$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$$h$:$T$$\rightarrow\mathbb{N}$. ($\forall$$x$:$T$. ($f$($x$) = $x$ $\in$ $T$) $\vee$ (($h$($f$($x$))) $<$ ($h$($x$))))